L:MsgA List. (A,BL.A ||+ B)  (AL. Feasible(A))  Feasible((L)) 

latex

Definitions	x:A. B(x), (L), reduce(f;k;as), Y, t  T, P  Q, (x,yL.P(x;y)), ||as||, Prop, x. t(x), AB, A, False, x,y. t(x;y), {i..j}, x(s), i  j < k, P & Q, P  Q, x(s1,s2)
Lemmas	msga wf, ma-empty-feasible, l all wf, ma-feasible wf, int seg wf, ma-compat wf, select wf, length wf2, pairwise-cons, l all cons, pairwise wf, ma-join-list-property